T:Type, ll:(T List) List, x:T.
(x  concat(ll))

(ll1, ll2:(T List) List, l1, l2:T List.
(concat(ll) = (concat(ll1) @ (l1 @ [x] @ l2) @ concat(ll2))  T List
(& ll = (ll1 @ [l1 @ [x] @ l2] @ ll2)) 

latex

Definitions	{T}, P  Q, SQType(T), , ij, ||as||, S  T, Top, x. t(x), concat(ll), as @ bs, Prop, t  T, x:A. B(x), P  Q, P  Q, P  Q, (x  l), x:A. B(x), P & Q
Lemmas	l member wf, iff wf, append wf, concat wf, member-concat, iff functionality wrt iff, all functionality wrt iff, append nil sq, concat-nil, concat-cons, top wf, concat append, member wf, length wf1, non neg length, nat wf, l member decomp, cons member, or functionality wrt iff, and functionality wrt iff, member append, iff transitivity